| Data transformation/Source transformation | |
|---|---|
| Concepts | |
| metadata · data mapping data transformation · model transf. |
|
| Languages | |
| ATL · AWK · MOFM2T · QVT · TXL XML languages |
|
| Techniques and transforms | |
| identity · synthesis · refinement | |
| Applications | |
| data migration · data conversion ETL · program transformation |
|
| Application fields | |
| Data warehouse Software engineering Software languages: macro, preprocessing, template |
|
Program synthesis is a special form of automatic programming that is most often paired with a technique for formal verification. The idea is to present human-understandable task specifications to a computer system and receive in return a program that is known to meet the specifications submitted.[1] The goal is, thus, to automatically construct a program that provably satisfies a given high-level specification. In contrast to other automatic programming techniques, the specifications are usually non-algorithmic statements of an appropriate logical calculus.[2]
Although it is hard to fully appreciate such an idea, given the intellectual accomplishment represented by it and its economical impact, once achieved, all the investment made over the years in this field, will eventually be repaid many times over.[1]
Contents |
Early developments in the field of constructive mathematics, saw the identification of algorithms with proofs (Kolmogorov, 1932). The advent automatic program synthesis systems, was shortly after the first theorem provers. Pioneer work was led by C. Green and R. Waldinnger, followed by transformational synthesis being introduced a few years later. Until the early 80's, program synthesis was a very vividly researched area. Some approaches were implemented and tested successfully, although none of them scaled up very well. As logic programming came into picture, the correctness problem appeared to be solved. The focus now shifted from the core activities of the field to the efficiency improvements. [3]
It was only after D. Smith began to incorporate the structural analysis of algorithmic classes into synthesis strategies, that large scale synthesis became possible[3]. The resulting KIDS project of D. Smith at Kestrel Institute, together with the associated research effort is a sophisticated example of constrained program synthesis concept. Its success can be accounted to the effectual use of algorithm schemata, design strategies and subsequent optimization techniques[1][3].
Program synthesis is closely related to the formal specification, which is the starting point of program synthesis. The specification is an expression in a formal language, having a syntax, a semantics and usually a proof theory. A good starting point involves the use declarative formalism, such as functional programming and computational logic, where one specifies what a program should do, rather than how. On one hand, the same logic can be used to express the specification, the resulting program and their relationship; on the other, logic specification may also be used to express incomplete specifications. Nevertheless, all the information can be expressed using the same language, and can therefore, be treated uniformly in a synthesis process[2]. The quality of the specification is fundamental to the output of the synthesis machine, which is a verified computer program[1][2].
Some feel that the concept of automated program generation often results in poor "factoring" of information. Known redundancy should be factored out, not introduced, it is said . However, sometimes specific programming languages are limited such that one has to introduce repetition of a concept or pattern in order to keep using the same language. Here is a simplified illustration of factoring:
Poor Factoring: x = a + a + a + a + a
Good Factoring: x = a * 5 (where the asterisk means "multiply")
Program generation tends to focus on automating the repetition seen in the first example, when a better approach is perhaps to find a higher-order abstraction, which is multiplication in this case. Other examples include putting parameters into a file or database instead of inside application code.